A, B:Type, eqa:(AA), eqb:(BB), f:(AB).
Inj(A;B;f)  RelsIso(A;B;x,y.(x eqa y);x,y.(x eqb y);f)  IsEqFun(B;eqb)  IsEqFun(A;eqa) 

latex

Up	gen algebra 1
Definitions of Statement	RelsIso(T;T';x,y.R(x;y);x,y.R'(x;y);f)
Definitions	x,y. t(x;y), , t  T, IsEqFun(T;eq), x f y, P  Q, x:A. B(x), P & Q, P  Q, P  Q, x(s1,s2), RelsIso(T;T';x,y.R(x;y);x,y.R'(x;y);f), Inj(A;B;f)
Lemmas	bool wf, inject wf, assert wf, rels iso wf, eqfun p wf, iff transitivity, iff functionality wrt iff